Chuẩn hóa

Từ 2 + 1 {\displaystyle 2+1} được rút gọn về 3 {\displaystyle 3} . Từ 3 {\displaystyle 3} không thể được rút gọn hơn nữa, nó được gọi là một dạng chuẩn. Một hệ hình thái được gọi là chuẩn hóa mạnh nếu tất cả các từ đều có dạng chuẩn và bất kỳ một dãy các phép rút gọn nào đều sẽ dẫn đến dạng chuẩn. Các hệ chuẩn hóa yếu là các hệ có dạng chuẩn, tuy nhiên các phép rút gọn có thể tạo thành vòng lặp và không dẫn đến dạng chuẩn.

Đối với một hệ chuẩn hóa, một phần tử là một lớp các từ có cùng một dạng chuẩn hóa. Một từ đóng là một từ không có tham số. (Một từ như x + 1 {\displaystyle x+1} với tham số x {\displaystyle x} được gọi là một từ mở.) Như vậy, 2 + 1 {\displaystyle 2+1} và 3 + 0 {\displaystyle 3+0} là hai từ khác nhau của phần tử 3 {\displaystyle 3} .

Các loại phụ thuộc

Một loại phụ thuộc là một loại mà phụ thuộc vào một từ hoặc loại khác. Ví dụ, loại trả về của một hàm có thể phụ thuộc vào đối số đưa vào hàm.

Ví dụ, một danh sách n a t {\displaystyle \mathrm {nat} } s có độ dài 4 có thể có loại khác với một danh sách n a t {\displaystyle \mathrm {nat} } s có độ dài 5.

Các loại đẳng thức

Nhiều hệ hình thái có một loại đại diện cho sự bằng nhau của các loại và các từ. Loại này khác với quy tắc chuyển đổi, và được gọi là đẳng thức mệnh đề.

Trong lý thuyết hình thái trực giác, loại đẳng thức được gọi là I {\displaystyle I} . Có một loại I   A   a   b {\displaystyle I\ A\ a\ b} với A {\displaystyle A} là một loại và a {\displaystyle a} , b {\displaystyle b} là các từ có loại A {\displaystyle A} . Một từ của loại I   A   a   b {\displaystyle I\ A\ a\ b} là một đẳng thức " a {\displaystyle a} bằng b {\displaystyle b} ".

Trong thực tế, có thể xây dựng một loại I   n a t   3   4 {\displaystyle I\ \mathrm {nat} \ 3\ 4} nhưng loại đó sẽ không có từ nào cả (vì 3 {\displaystyle 3} khác 4 {\displaystyle 4} ). Trong lý thuyết loại trực giác, ta xây dựng các từ đẳng thức bắt đầu từ các đẳng thức đồng nhất. Nếu 3 {\displaystyle 3} là một từ loại n a t {\displaystyle \mathrm {nat} } , tồn tại một từ với loại I   n a t   3   3 {\displaystyle I\ \mathrm {nat} \ 3\ 3} . Các đẳng thức phức tạp hơn có thể được tạo ra bằng cách tạo ra một từ đồng nhất rồi thực hiện rút gọn một bên. Ví dụ, nếu 2 + 1 {\displaystyle 2+1} là một từ loại n a t {\displaystyle \mathrm {nat} } , ta có một đẳng thức đồng nhất I   n a t   ( 2 + 1 )   ( 2 + 1 ) {\displaystyle I\ \mathrm {nat} \ (2+1)\ (2+1)} , và bằng cách rút gọn, ta có một từ mới loại I   n a t   ( 2 + 1 )   3 {\displaystyle I\ \mathrm {nat} \ (2+1)\ 3} . Do đó, trong hệ này, loại đẳng thức thể hiện rằng hai giá trị cùng loại có thể được chuyển đổi bằng phép rút gọn.